COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	DECLARE PREDPAR P(ORDINAL) Q(NATNUM)
C00004 ENDMK
C⊗;
DECLARE PREDPAR P(ORDINAL) Q(NATNUM);

DECLARE INDVAR M M0 M1 M2 N N1 N2 ε NATNUM;

DECLARE INDVAR X X0 X1 Y Y0 Y1 ε ORDINAL;

DECLARE PREDCONST <(NATNUM,NATNUM) [L←450,R←475];

AXIOM INDUCTION:
	∀N.(∀M.(M < N ⊃ P(M)) ⊃ P(N)) ⊃ ∀N.P(N);;

DECLARE OPCONST SUCC(NATNUM) = NATNUM;

DECLARE PREDCONST LESS(ORDINAL,ORDINAL) [L←450,R←475];

DECLARE OPCONST LPOW(ORDINAL) = NATNUM;

DECLARE OPCONST LCOEF(ORDINAL) = NATNUM;

DECLARE OPCONST TAIL(ORDINAL);

AXIOM TAIL:
	∀X.((NULL TAIL X ∨ ISORDINAL TAIL X) ∧ ¬(NULL TAIL X ∧ ISORDINAL TAIL X))
	∀X.(ISORDINAL TAIL X ⊃ LPOW TAIL X < LPOW X
;;

AXIOM LESS:
	∀X Y.(LPOW X < LPOW Y ⊃ X LESS Y)
	∀X Y.(LPOW X = LPOW Y ∧ LCOEF X < LCOEF Y ⊃ X LESS Y)
	∀X Y.(LPOW X = LPOW Y ∧ LCOEF X = LCOEF Y ∧ NULL TAIL X
∧ NULL TAIL Y ⊃ X = Y)
	∀X Y.(LPOW X = LPOW Y ∧ LCOEF X = LCOEF Y ∧ NULL TAIL X
∧ ¬(NULL TAIL Y) ⊃ X LESS Y)
	∀X Y.(LPOW X = LPOW Y ∧ LCOEF X = LCOEF Y ∧ ISORDINAL TAIL X
∧ ISORDINAL TAIL Y ⊃ (X LESS Y ≡ TAIL X LESS TAIL Y)
	∀X Y.(X LESS Y ∨ X = Y ∨ Y LESS X)
;;